(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(push)
(declare-const v4 Bool)
(declare-const r1 Real)
(pop)
(declare-const v5 Bool)
(declare-const r2 Real)
(declare-const r3 Real)
(push)
(declare-const r4 Real)
(declare-const v6 Bool)
(declare-const v7 Bool)
(pop)
(declare-const v8 Bool)
(declare-const v9 Bool)
(assert (forall ((q0 Bool) (q1 Bool) (q2 Real)) (=> (> r3 q2 q2 q2 r2) (distinct q1 q1 v8))))
(declare-const r5 Real)
(push)
(declare-const v10 Bool)
(assert (exists ((q3 Real) (q4 Real)) (distinct r2 (- 12.0) (- 12.0))))
(pop)
(push)
(declare-const v11 Bool)
(declare-const v12 Bool)
(push)
(declare-const r6 Real)
(declare-const r7 Real)
(pop)
(declare-const v13 Bool)
(assert (or (<= r3 (* (- 12.0) r2 12.0) 12.0) (distinct r2 (- 12.0) (- 12.0)) v8 (>= (* (- 12.0) r2 12.0) 12.0 (* (- 12.0) r2 12.0)) v3))
(assert (or v5 (distinct r2 r5 r3 (- 12.0) r3) v3))
(assert (or (distinct (* r2 (- 12.0)) r2 r2 (* (- 12.0) r2 12.0) (- 12.0))))
(assert (or (>= (* (- 12.0) r2 12.0) 12.0 (* (- 12.0) r2 12.0)) (< r3 (- 12.0) (- 12.0) r2)))
(assert (or v8))
(assert (or v0))
(assert (or v1 v2 v1 (not v9) v5 v5 v0))
(assert (or v0))
(check-sat)
